Inference at * 
Iof proof for Lemma hd member:


  T:Type, L:(T List). ((null(L)))  (hd(L)  L) 

latex

 by Auto THEN DVar `L' THEN All Reduce THEN MaAuto 

latex

 1: 

 1: 1. T : Type
 1: 2. True
 1:   ([]  [])
 .

Definitions	null(as), b, True, last(L), P  Q, P  Q, P  Q, left + right, [], [car / cdr], A List, , , {i..j}, {x:A| B(x)} , i  j < k, P & Q, i  j , n+m, ||as||, x:A. B(x), #$n, False, P  Q, x:AB(x), Void, , s = t, t  T, a < b, A  B, x:A  B(x), (x  l), A, type List, s ~ t, Type, l[i], i z j, i <z j, hd(l)
Lemmas	l member wf, not wf, assert wf, null wf, select member, nat wf, int seg wf, member wf, non neg length, length wf1, le wf